\section{Лямбда-исчисление}

$$
\begin{array}{rcl}
X&=&\{x, y, z, \dots\} \mbox{ --- счетно-бесконечное множество переменных}\\
\Lambda&=& X \mid \Lambda\Lambda \mid \lam{X}{\Lambda}
\end{array}
$$

Соглашения о скобках: применение левоассоциативно, абстракция ``жаднее'' 
применения.

Свободные переменные:

$$
\begin{array}{rcl}
  FV(x)&=&\{x\}\\
  FV(AB)&=&FV(A)\cup FV(B)\\
  FV(\lam{x}{A})&=&FV(A)\setminus \{x\}
\end{array}
$$

Подстановка:

$$
\begin{array}{rcl}
  x[x\gets N]&=&N\\
  y[x\gets N]&=&y,\:y\ne x\\
  (AB)[x\gets N]&=&A[x\gets N]B[x\gets N]\\
  (\lam{x}{A})[x\gets N]&=&\lam{x}{A}\\
  (\lam{y}{A})[x\gets N]&=&\lam{y}A[x\gets N],\:y\notin FV(N)\mbox{ или }y\notin FV(A)
\end{array}
$$

$\alpha$-конверсия: 

$$
\aconv{\lam{x}{A}}{x\gets y}{\lam{y}{(A[x\gets y])}},\:y\notin FV(A)
$$

$\alpha$-конверсию можно превратить в отношение эквивалентности ``$\asim{}{}$''.
Сперва будем считать, что 

$$
\asim{\lam{x}{A}}{\lam{y}{B}}\Leftrightarrow\aconv{\lam{x}{A}}{x\gets y}{B}
$$

Это отношение симметрично и транзитивно, можно его дополнить до рефлексивного,
а потом распространить на лямбда-термы остальных видов:

$$
\begin{array}{rcl}  
  \asim{A}{A^\prime}&\Rightarrow&\asim{AB}{A^\prime}{B}\\
  \asim{B}{B^\prime}&\Rightarrow&\asim{AB}{A}{B^\prime}\\
  \asim{A}{A^\prime}&\Rightarrow&\asim{\lam{x}{A}}{\lam{x}{A^\prime}}
\end{array}
$$

Теперь можно ``починить'' подстановку, сделав её возможной всегда:

$$
\begin{array}{c}
(\lam{y}{A})[x\gets N]=\lam{z}{A^\prime[x\gets N]},\:y\in FV(N)\mbox{ и }y\in FV(A)\\
\mbox{где }\aconv{\lam{y}{A}}{y\gets z}{\lam{z}{A^\prime}}\mbox{ и }z\notin FV(N)
\end{array}
$$

$\beta$-редукция: 

$$
  \bred{(\lam{x}{A})B}{A[x\gets B]}
$$

Нормальный порядок редукций:

$$
\trans{x}{}{x}\ruleno{Var$^{no}_{bs}$}
$$

$$
\trule{\trans{A}{}{A^\prime}}
      {\trans{\lam{x}{A}}{}{\lam{x}{A^\prime}}}\ruleno{Abstr$^{no}_{bs}$}
$$

$$
\trule{\trans{A[x\gets B]}{}{B^\prime}}
      {\trans{(\lam{x}{A})B}{}{B^\prime}}\ruleno{Beta$^{no}_{bs}$}
$$

$$
\crule{\trans{A}{}{\lam{x}{A^\prime}};\;\trans{A^\prime[x\gets B]}{}{C}}
      {\trans{AB}{}{C}}
      {A\mbox{ --- не абстракция}}\ruleno{App-Beta$^{no}_{bs}$}
$$

$$
\crule{\trans{A}{}{A^\prime};\;\trans{B}{}{B^\prime}}
      {\trans{AB}{}{A^\prime B^\prime}}
      {A^\prime\mbox{ --- не абстракция}}\ruleno{App$^{no}_{bs}$}
$$

При нормальном порядке редукций редуцируется самый внешний, самый левый
редекс (можно обосновать, глядя на правила). При нормальном порядке
редукций либо получается нормальная форма, либо процесс редуцирования
не завершается (пример --- $(\lam{x}{xx})\lam{x}{xx}$). В нормальной
форме больше нет редексов (если бы был хоть один, то был бы и самый
внешний самый левый). Можно вывести синтаксический вид нормальной формы:

$$
\begin{array}{rcl}
  N &=&X \mid \lam{X}{N} \mid N_A \\
  N_A&=& XN \mid N_AN_A
\end{array}
$$

Call-by-name:

$$
\trans{x}{}{x}\ruleno{Var$^{cbn}_{bs}$}
$$

$$
\trans{\lam{x}{A}}{}{\lam{x}{A}}\ruleno{Abstr$^{cbn}_{bs}$}
$$

$$
\trule{\trans{A}{}{\lam{x}{A^\prime}};\;\trans{A^\prime[x\gets B]}{}{C}}
      {\trans{AB}{}{C}}\ruleno{Beta$^{cbn}_{bs}$}
$$

$$
\crule{\trans{A}{}{A^\prime}}
      {\trans{AB}{}{A^\prime B}}
      {A^\prime\mbox{--- не абстракция}}\ruleno{App$^{cbn}_{bs}$}
$$

То, что получается в результате редукции по стратегии call-by-name, называется
\emph{слабозаголовочной нормальной формой} (\emph{weak head normal form}). Её
можно описать следующим образом:

$$
\begin{array}{rcl}
N^{wh}&=&N^{wh}_a\mid \lam{X}{\Lambda}\\
N^{wh}_a&=&X\mid N^{wh}_a\Lambda
\end{array}
$$

Call-by-value:

$$
\trans{x}{}{x}\ruleno{Var$^{cbv}_{bs}$}
$$

$$
\trans{\lam{x}{A}}{}{\lam{x}{A}}\ruleno{Abstr$^{cbv}_{bs}$}
$$

$$
\trule{\trans{A}{}{\lam{x}{A^\prime}};\;\trans{B}{}{B^\prime},\;\trans{A^\prime[x\gets B^\prime]}{}{C}}
      {\trans{AB}{}{C}}\ruleno{Beta$^{cbv}_{bs}$}
$$

$$
\crule{\trans{A}{}{A^\prime};\;\trans{B}{}{B^\prime}}
      {\trans{AB}{}{A^\prime B^\prime}}
      {A^\prime\mbox{--- не абстракция}}\ruleno{App$^{cbv}_{bs}$}
$$

В результате получается \emph{слабая нормальная форма} (\emph{weak normal form}), 
которая имеет вид

$$
\begin{array}{rcl}
N^w&=&N^w_a\mid \lam{X}{\Lambda}\\
N^w_a&=&X\mid N^w_aN^w_a
\end{array}
$$

\subsection{Представление де-Брауна}

Представление \emph{де-Брауна} (\emph{De Bruijn nameless representation})~---
подход, при котором вместо имени связанной переменной используется номер
символа $\lambda$, которым эта переменная связана (считая изнутри-вовне, или
справа-налево). Формально,

$$
\Lambda^N=\mathbb{N} \mid \Lambda^N\Lambda^N \mid \lamN{\Lambda^N}
$$

При этом вхождению свободной переменной соответствует номер, больше или равный 
максимальному уровню вложенности данного вхождения в $\lambda$-абстракции.

Проще всего --- на примерах:

\begin{table}[!ht]
\centering
\begin{tabular}{c|c}
$\Lambda$ & $\Lambda^N$\\
\hline
$\lam{x}{x}$&$\lamN{0}$\\
$\lam{x}{\lam{y}{yx}}$&$\lamN{\lamN{01}}$\\
$\lam{x}{\lam{y}{yx\lam{z}{yzx}}}$&$\lamN{\lamN{01\lamN{102}}}$
\end{tabular}
\caption{Примеры представления де-Брауна для некоторых $\lambda$-термов}
\label{deBruijnExample}
\end{table}

В последнем примере хорошо видно, как индекс одной и той же переменной (например, $x$)
увеличивается по мере того, как она ``погружается'' во вложенные абстракции.

Понятно, что поскольку в представлении де-Брауна имен переменных нет, то, во-первых,
$\alpha$-эквивалентные термы без свободных переменных будут представлены одинаково, 
и, во-вторых, не будет никаких конфликтов из-за имён переменных при подстановках (если, 
конечно, научиться делать подстановки для данного представления).

Сперва научимся превращать обычные термы в термы де-Брауна. Всё, что для этого
понадобится~--- это поддержание упорядоченного списка переменных $\inbr{x,y,\dots}$ с операцией ``$?$''
взятия номера какой-либо переменной в этом списке. Например: $\inbr{a,b,c}?a=0$, $\inbr{a,b,c}?b=1$ и т.д.
Будем считать, что самой левой переменной соответствует позиция $0$; так как, вообще говоря, переменные
могут повторяться, условимся, что ``$?$'' возвращает номер самого левого её вхождения. Тогда
преобразование обычного терма в форму де-Брауна можно записать следующим образом:

$$
\withenv{\Gamma}{\trans{x}{}{\Gamma?x}}\ruleno{Var$^{\to N}$}
$$

$$
\trule{\withenv{\Gamma}{\trans{M}{}{M^\prime}},\:\withenv{\Gamma}{\trans{N}{}{N^\prime}}}{\withenv{\Gamma}{\trans{MN}{}{M^\prime N^\prime}}}\ruleno{App$^{\to N}$}
$$

$$
\trule{\withenv{x:\Gamma}{\trans{A}{}{A^\prime}}}{\withenv{\Gamma}{\trans{\lam{x}{A}}{}{\lamN{A^\prime}}}}\ruleno{Abstr$^{\to N}$}
$$

Теперь если $A$~--- замкнутый терм и $\withenv{\inbr{\;}}{\trans{A}{}{A^\prime}}$, то $A^\prime$~--- его
представление в форме де-Брауна.

Аналогично, чтобы из представления де-Брауна получить ``обычные'' термы, надо, во-первых, иметь
достаточный ``запас'' имен переменных и, во-вторых, помнить, какой переменной соответствует 
данное вхождение целочисленного индекса:

$$
\withenv{V,\:\Gamma}{\trans{i}{}{\Gamma\:[i]}}\ruleno{Var$^{\gets N}$}
$$

$$
\trule{\withenv{V,\;\Gamma}{\trans{M}{}{M^\prime}},\;\withenv{V,\;\Gamma}{\trans{N}{}{N^\prime}}}{\withenv{V,\;\Gamma}{\trans{MN}{}{M^\prime N^\prime}}}\ruleno{App$^{\gets N}$}
$$

$$
\trule{\withenv{V,\;x:\Gamma}{\trans{A}{}{A^\prime}}}{\withenv{x:V,\:\Gamma}{\trans{\lamN{A}}{}{\lam{x}{A^\prime}}}}\ruleno{Abstr$^{\gets N}$}
$$

Здесь $\Gamma\:[i]$~--- взятие $i$-го элемента из списка $\Gamma$, $V$~--- упорядоченный бесконечный список переменных. Теперь если
$A^\prime$~--- терм в форме де-Брауна и $\withenv{V,\;\inbr{\;}}{\trans{A^\prime}{}{A}}$, то $A$~--- его обычное представление.

Осталось разобраться с тем, как осуществлять подстановку в представлении де-Брауна. Случаи применения и переменной~--- тривиальны:

$$
\begin{array}{rcl}
  i[i\gets A]&=&A\\
  j[i\gets A]&=&j,\;i\ne j\\
  (MN)[i\gets A]&=&M[i\gets A]N[i\gets A]
\end{array}
$$

Остался случай абстракции. Важно сообразить, что если мы производим подстановку $\lamN{M}[i\gets A]$, то индексы, соответствующие
связанным вхождениям переменных в $A$, не меняются, а свободным~--- увеличиваются на единицу (потому, что мы ``втаскиваем'' $A$
под ``$\lambda$''). Кроме того, мы хотим заменить в терме $\lamN{M}$ все свободные вхождения переменной с индексом $i$; но
такие вхождения в $M$ соответствуют уже индексу $i+1$ (потому, что в терме $\lamN{M}$ $M$ стоит под ``$\lambda$''). Итого:

$$
(\lamN{M})[i\gets A]=\lamN{(M[i+1\gets\left\uparrow A\right.])}
$$

где $\left\uparrow A\right.$~--- операция увеличения индексов всех свободных вхождений переменных в $A$. 

Что в точности делает ``$\left\uparrow A\right.$''? Она ``пробирается'' внутрь $A$ и инкрементирует все
свободные вхождения переменных. Поскольку свободные вхождения~--- это все те, чьи индексы превышают
уровень вложенности в ``$\lambda$'', этот уровень нужно аккуратно считать. Итого:

$$
\begin{array}{rcl}
   \left\uparrow A\right.&=&\left\uparrow^0A\right.\\
   \left\uparrow^l(MN)\right.&=&(\left\uparrow^lM\right.)(\left\uparrow^lN\right.)\\
   \left\uparrow^li\right.&=&\left\{\begin{array}{rcl}
                                      i+1&,&i>l\\
                                      i&,&i\le l
                                    \end{array}
                             \right.\\
   \left\uparrow^l(\lamN{A})\right.&=&\lamN{(\left\uparrow^{l+1}A\right.)}
\end{array}
$$

Вот и всё.

Доказать, что $\alpha$-эквивалентные термы имеют одно и то же представление де-Брауна.
И подстановка тоже сохраняет свой смысл (то есть, что если подставить по старым
правилам, а потом преобразовать в де-Брауна и подставить по де-Брауновским и сконвертировать
обратно, получится $\alpha$-эквивалентный терм).

\subsection{Замыкания}

Дальше будем рассматривать еще более ограниченную стратегию редукций, а именно~--- если
в применении ``левая'' часть не редуцируется в абстракцию, то процесс останавливается
(это строго говоря не call-by-name(value), но больше соответствует поведению функциональных
программ).

Можно заметить, что индексы де-Брауна можно использовать для того, чтобы ``добираться''
до значений нужных свободных переменных в процессе редукции. Если $C$~--- вектор
из $\lambda$-термов, то $C[i]$~--- это ``значение'' $i$-го индекса де-Брауна. 
Таким образом, можно вообще отказаться от подстановки термов, если к каждой
редуцируемой абстракции присоединять тот вектор, который был в наличии в момент редукции.
Такой вектор называется \emph{замыканием} (\emph{closure}). При наличии
замыканий семантика call-by-name выглядит так:

$$
\withenv{C}{\trans{i}{}{C\,[i]}}\ruleno{Var$^{cbn}_c$}
$$

$$
\withenv{C}{\trans{\lamN{A}}{}{\lamN{A}\,[C]}}\ruleno{Abstr$^{cbn}_c$}
$$

$$
\trule{\withenv{C}{\trans{A}{}{\lamN{A^\prime}\,[C^\prime]}},\;\withenv{B:C^\prime}{\trans{A^\prime}{}{C}}}
      {\withenv{C}{\trans{AB}{}{C}}}\ruleno{App$^{cbn}_c$}
$$

А call-by-value~--- так:

$$
\withenv{C}{\trans{i}{}{C\,[i]}}\ruleno{Var$^{cbv}_c$}
$$

$$
\withenv{C}{\trans{\lamN{A}}{}{\lamN{A}\,[C]}}\ruleno{Abstr$^{cbv}_c$}
$$

$$
\trule{\withenv{C}{\trans{A}{}{\lamN{A^\prime}\,[C^\prime]}},\;\withenv{C}{\trans{B}{}{B^\prime}},\;\withenv{B^\prime:C^\prime}{\trans{A^\prime}{}{C}}}
      {\withenv{C}{\trans{AB}{}{C}}}\ruleno{App$^{cbv}_c$}
$$

Ну и доказать, что ничего не портится.

\subsection{Обогащение $\lambda$-исчисления}

Добавим к чистому исчислению целые числа и тэгированные значения:

$$
{\cal C}=\{C^{n_1}_1, C^{n_2}_2,\dots\}\;\mbox{ --- счетно-бесконечное семейство конструкторов}
$$

Здесь $C^{n_i}_i$~--- конструктор арности $n_i$. Множество значений:

$$
{\cal V}=\mathbb{Z}\cup \Lambda\cup\bigcup_{\cal C}{C^{n_i}_i{\cal V}^{n_i}}
$$

Обогащенный язык: константы, бинарные операции, конструкторы, сопоставление
с образцом. Семантика большого шага, $\delta$-правила.

Let-определения, рекурсия, взаимная рекурсия. Семантика и синтаксические сокращения.

\subsection{SECD--машина}

Стек, код, окружение. Система команд:

\begin{enumerate}
  \item \cd{ACCESS($n$)}~--- положить $n$-й элемент окружения на стек;
  \item \cd{CLOSURE($c$)}~--- положить на стек замыкание кода $c$;
  \item \cd{LET}~--- снять вершину стека и положить её в начало окружения;
  \item \cd{ENDLET}~--- ``сбросить'' первый элемент окружения;
  \item \cd{APPLY}~--- применить замыкание функции к аргументу (и то, и другое должны
лежать на вершине стека);
  \item \cd{RETURN}~--- вернуться из функции.
\end{enumerate}

Операционная семантика большого шага:

$$
\withenv{e}{\trans{s}{\mbox{$\epsilon$}}{s}}\ruleno{EMPTY$^{SECD}$}
$$

$$
\trule{\withenv{e}{\trans{e(n):s}{\mbox{$c$}}{s^\prime}}}
      {\withenv{e}{\trans{s}{\mbox{\cd{ACCESS($n$)};$\:c$}}{s^\prime}}}\ruleno{Access$^{SECD}$}
$$

$$
\trule{\withenv{x:e}{\trans{s}{\mbox{$c$}}{s^\prime}}}
      {\withenv{e}{\trans{x:s}{\mbox{\cd{LET};$\:c$}}{s^\prime}}}\ruleno{Let$^{SECD}$}
$$

$$
\trule{\withenv{e}{\trans{s}{\mbox{$c$}}{s^\prime}}}
      {\withenv{x:e}{\trans{s}{\mbox{\cd{ENDLET};$\:c$}}{s^\prime}}}\ruleno{EndLet$^{SECD}$}
$$

$$
\trule{\withenv{e}{\trans{c^\prime[e]:s}{\mbox{$c$}}{s^\prime}}}
      {\withenv{e}{\trans{s}{\mbox{\cd{CLOSURE($c^\prime$)};$\:c$}}{s^\prime}}}\ruleno{Closure$^{SECD}$}
$$

$$
\trule{\withenv{x:e^\prime}{\trans{c:e:s}{\mbox{$c^\prime$}}{s^\prime}}}
      {\withenv{e}{\trans{x:c^\prime[e^\prime]:s}{\mbox{\cd{APPLY};$\:c$}}{s^\prime}}}\ruleno{Apply$^{SECD}$}
$$

$$
\trule{\withenv{e^\prime}{\trans{x:s}{\mbox{$c^\prime$}}{s^\prime}}}
      {\withenv{e}{\trans{x:c^\prime:e^\prime:s}{\mbox{\cd{RETURN};$\:c$}}{s^\prime}}}\ruleno{Return$^{SECD}$}
$$

Транслятор:

$$
\begin{array}{rcl}
  \sembr{i}&=&\mbox{\cd{ACCESS($i$)}}\\
  \sembr{\lamN{A}}&=&\mbox{\cd{CLOSURE($\sembr{A}$)}; \cd{RETURN}}\\
  \sembr{\mbox{\cd{let $A$ in $B$}}}&=&\sembr{A};\:\mbox{\cd{LET}};\:\sembr{B};\:\mbox{\cd{ENDLET}}\\
  \sembr{A\:B}&=&\sembr{A};\:\sembr{B};\:\mbox{\cd{APPLY}}
\end{array}
$$

